b:. (b)  (Ax  (b)) 

latex

ProofTree

Definitions	left + right, P  Q, P & Q, x:A  B(x), , s = t, b, A, , x:AB(x), b, Unit, False, True, , P  Q, Ax, x:A. B(x), , t  T, #$n
Lemmas	member wf, false wf, it wf, true wf, bool wf, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert